COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Comments on ekl
C00008 ENDMK
C⊗;
Comments on ekl

How is ekl's logic weaker than set theory?

1. We cannot form finite sets of object of arbitrary types?  Can we
form sets by enumeration of elements without making axioms?

2. By the way, what are ekl's facilities for making definitions
and distinguishing them from axioms?

3. foo#ldg  may be a too ad hoc use of  #  as a separator.
FOL suffers from randomness in the assignment of separators.

4. How about allowing file names to be referred to in the conventional
syntax by writing |file.ext[proj,prog]|?

5. How aobut preparing proofs with the editor and reading them in,
i.e. as lists of commands can be prepared in FOL and fetched.  It
is especially convenient to treat axioms this way.

6. error on p.16 line 3 of may 31 Weening manual. ¬D should be D

7. omission of vowels is undesirable.  TRMREWRITE should be TERMREWRITE.

8. It would be nice if  deletel told what had been deleted.

9. Is there any way to edit a proof?  I defined  nil  as a constant,
and it seemed to work, but later it became clear that it hadn't worked.
Must I pretty-print the proof, edit the result, deleting ekl's replies
and re-arrange the lines I want re-arranged, then telnet to saii and
log in to ekl and then feed ekl the edited input lines using the feature
of telnet to take input from a file?

Aug 15

Definitions instead of axioms

We have been introducing LISP functions by axioms.  This is not right,
because with an axiom one can say something false or even contradictory.
It would be better if LISP functions were introduced by definitions, which
EKL would check to see if they are properly conservative.  Ideally, the
writer of a program would use an EKL that allowed him to make definitions
but which did not allow him to introduce new axioms.  If he then
defined some functions and proved that they had certain properties,
one could believe it and pay him, modulo errors in the design of EKL
or in the axioms provided with the EKL system and by the potential purchaser
of the LISP programs.

Present LISP recursive definitions cannot be accepted as definitions
by FOL or EKL, because the function being defined occurs on both sides
of the equation.  There are several possible solutions.

1. The simplest, in a form suggested by me and Carolyn Talcott, is to
allow several flavors of Y combinator, each suitably axiomatized in
the EKL LISP axioms.  Once these Y combinators are supplied and
axiomatized, the EKL definition mechanism should accept definitions
of LISP functions, because they are no longer recursive, i.e. their
right hand sides don't contain the function name being defined but
suitable λ-expressions giving functionals of which the Y operator
specifies the minimal fixed points.  Carolyn Talcott's idea is that
some of them provide the machinery for primitive recursive definitions
of various kinds, which are then automatically terminate, i.e. automatically
have lists or S-expressions as their range.  These would be used
when applicable.  Otherwise, the programmer would use the general
mechanism and would have to prove termination.

2. More elaborately, the definition facility of EKL would have to
be elaborated to accept certain definitions in which the function
being defined also appears on the right hand side.  A large class
of these can be shown to be allowable when the domain and range
are cartesian product of GROUNDs and GROUND respectively.  Then
the definition is satisfied by taking the value to be bottom.
[This paragraph is not correctly formulated yet].